M1, M2:MsgA.
M1  M2
 (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x). M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w)) 

latex

Definitions	t  T, IdDeq, x:A. B(x), Id, Top, P  Q, f(x)?z, x. t(x), Prop, Knd, 2of(t), A & B, f  g, IdLnk, State(ds), 1of(t), f(x), a:A fp B(a), KindDeq, product-deq(A;B;a;b), x  dom(f), b, z != f(x)  P(a;z), P & Q, Valtype(da;k), MsgA, M1  M2, M.state, M.da(a), M.ds(x), M.ef(k,x,s,v,w)
Lemmas	msga wf, ma-sub wf, ma-st wf, ma-da wf, ma-ds wf, assert wf, fpf-dom wf, product-deq wf, Kind-deq wf, fpf-trivial-subtype-top, ma-state wf, pi1 wf, fpf-ap wf, pi2 wf, Knd wf, fpf-cap-void-subtype, fpf-cap wf, subtype-fpf-cap-top, top wf, Id wf, id-deq wf